/*!
 * \file set_relation_test.cc
 *
 * \brief Set and Relation tests
 *
 * This file is to test all of the Set and Relation classes, along with the
 * related classes: SREquality, SRInequality, and SRConjunction
 *
 * \date Started: 6/8/2010
 * \date Last Modified: 7/27/2010
 * \authors Alan LaMielle
 * \authors Ian Craig
 */

#include <iegenlib/iegenlib.h>

#include <gtest/gtest.h>
#include <utility>
using std::pair;
using std::make_pair;
#include <iostream>
using std::cout;
using std::endl;

using iegenlib::TUPLE;
using iegenlib::EXISTENTIAL;
using iegenlib::SYMBOLIC;
using iegenlib::UFCALL;
using iegenlib::CONST;

using iegenlib::IEGenLibContext;
using iegenlib::Set;
using iegenlib::Relation;
using iegenlib::TupleType;
using iegenlib::SymbolTable;
using iegenlib::ExpVec;
using iegenlib::SREquality;
using iegenlib::SRInequality;
using iegenlib::SRConjunction;
using iegenlib::UFCall;
using iegenlib::Symbolic;

//This is just a test setup class that is used in the other tests in this
//file. It creates a symbol table with 3 of each type of variable for
//the test cases to use so that we don't have to repeat the symbol table
//creation each time.
class SparseConstraintTest:public::testing::Test{
public:
  SymbolTable* st;
  list<TupleType> tuples;
  list<string> all;
protected:
  virtual void SetUp(){
    set<string> varTuple;
    varTuple.insert("var1");
    all.push_back("var1");
    varTuple.insert("var2");
    all.push_back("var2");
    varTuple.insert("var3");
    all.push_back("var3");
    set<string> symbolics;
    symbolics.insert("sym1");
    all.push_back("sym1");
    symbolics.insert("sym2");
    all.push_back("sym2");
    symbolics.insert("sym3");
    all.push_back("sym3");
    set<string> exists;
    exists.insert("exist1");
    all.push_back("exist1");
    exists.insert("exist2");
    all.push_back("exist2");
    exists.insert("exist3");
    all.push_back("exist3");
    list<pair<string, int> > conVal;
    st = new SymbolTable(&varTuple, &symbolics, &exists, 3);
    st->lookup("f()",list<ExpVec>());
    all.push_back("f()");
    st->lookup("g()",list<ExpVec>());
    all.push_back("g()");
    st->lookup("h()",list<ExpVec>());
    all.push_back("h()");

    tuples.push_back(TupleType("var1"));
    tuples.push_back(TupleType("var2"));
    tuples.push_back(TupleType("var3"));
  }

  virtual void TearDown(){
    delete st;
  }
};

//Test the SRConstraint.any() method
TEST_F(SparseConstraintTest, ConstraintAny){
  set<string> varTuple;
  varTuple.insert("var1");
  set<string> symbolics;
  set<string> exists;
  exists.insert("exist1");
  exists.insert("exist3");
  list<pair<string, int> > conVal;
  SymbolTable st(&varTuple, &symbolics, &exists, 2);

  ExpVec v=st.constructExpVec();
  SREquality eq(v);
  SRInequality ineq(v);
  int pos,coeff;
  bool res;

  //No coefficients have been set
  EXPECT_EQ(eq.any(SYMBOLIC,pos,coeff),false);
  EXPECT_EQ(eq.any(TUPLE,pos,coeff),false);
  EXPECT_EQ(eq.any(EXISTENTIAL,pos,coeff),false);
  EXPECT_EQ(eq.any(UFCALL,pos,coeff),false);
  EXPECT_EQ(eq.any(CONST,pos,coeff),false);

  EXPECT_EQ(ineq.any(SYMBOLIC,pos,coeff),false);
  EXPECT_EQ(ineq.any(TUPLE,pos,coeff),false);
  EXPECT_EQ(ineq.any(EXISTENTIAL,pos,coeff),false);
  EXPECT_EQ(ineq.any(UFCALL,pos,coeff),false);
  EXPECT_EQ(ineq.any(CONST,pos,coeff),false);

  //Just var1=1 has been set
  v=st.constructExpVec("var1",1);
  eq=SREquality(v);
  ineq=SRInequality(v);
  EXPECT_EQ(eq.any(SYMBOLIC,pos,coeff),false);
  EXPECT_EQ(eq.any(EXISTENTIAL,pos,coeff),false);
  EXPECT_EQ(eq.any(UFCALL,pos,coeff),false);
  EXPECT_EQ(eq.any(CONST,pos,coeff),false);
  res=eq.any(TUPLE,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,0);
  EXPECT_EQ(coeff,1);

  EXPECT_EQ(ineq.any(SYMBOLIC,pos,coeff),false);
  EXPECT_EQ(ineq.any(EXISTENTIAL,pos,coeff),false);
  EXPECT_EQ(ineq.any(UFCALL,pos,coeff),false);
  EXPECT_EQ(ineq.any(CONST,pos,coeff),false);
  res=ineq.any(TUPLE,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,0);
  EXPECT_EQ(coeff,1);

  //exist1=-6, ufcall 1 = 3, and const=22
  v.set_coeff(EXISTENTIAL,0,-6);
  v.set_coeff(UFCALL,1,3);
  v.set_const(22);
  eq=SREquality(v);
  ineq=SRInequality(v);

  EXPECT_EQ(eq.any(SYMBOLIC,pos,coeff),false);
  res=eq.any(TUPLE,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,0);
  EXPECT_EQ(coeff,1);
  res=eq.any(EXISTENTIAL,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,0);
  EXPECT_EQ(coeff,-6);
  res=eq.any(UFCALL,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,1);
  EXPECT_EQ(coeff,3);
  res=eq.any(CONST,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(coeff,22);
  EXPECT_EQ(ineq.any(SYMBOLIC,pos,coeff),false);
  res=ineq.any(TUPLE,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,0);
  EXPECT_EQ(coeff,1);
  res=ineq.any(EXISTENTIAL,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,0);
  EXPECT_EQ(coeff,-6);
  res=ineq.any(UFCALL,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(pos,1);
  EXPECT_EQ(coeff,3);
  res=ineq.any(CONST,pos,coeff);
  EXPECT_TRUE(res);
  EXPECT_EQ(coeff,22);
}

//This tests the SREquality class and all of its methods except for the apply
//methods for the tree.
//Methods Tested:
//Less than operator:
//   The less than operator works by calling the less than operator on the
//   Equality's Expression Vectors
//Equal to operator:
//   The equal to operator works in a similar fashion by calling the said
//   operator on the Equality's Expression Vectors
TEST_F(SparseConstraintTest, EqualityTests){
  ExpVec EV1 = st->constructExpVec("var1", 4);
  ExpVec EV2 = st->constructExpVec("sym2", 3);
  ExpVec EV3 = st->constructExpVec("exist3", 2);
  ExpVec EV4 = st->constructExpVec("f()",list<ExpVec>(), 1);
  SREquality eq1(EV1);
  SREquality eq2(EV2);
  EXPECT_TRUE(eq1 < eq2); //Tests the less than operator
  SREquality eq1_2(EV1);
  EXPECT_TRUE(eq1 == eq1_2); //Tests the equal to operator
}

//This tests the SRInequality class and all of its methods except for the apply
//methods for the tree.
//Methods Tested:
//Less than operator:
//   The less than operator works by calling the less than operator on the
//   Inequality's Expression Vectors
//Equal to operator:
//   The equal to operator works in a similar fashion by calling the said
//   operatro on the Inequality's Expression Vectors
TEST_F(SparseConstraintTest, InequalityTests){
  ExpVec EV1 = st->constructExpVec("var1", 4);
  ExpVec EV2 = st->constructExpVec("sym2", 3);
  ExpVec EV3 = st->constructExpVec("exist3", 2);
  ExpVec EV4 = st->constructExpVec("f()",list<ExpVec>(), 1);
  SRInequality ineq1(EV1);
  SRInequality ineq2(EV2);
  EXPECT_TRUE(ineq1 < ineq2);  //Tests the less than operator
  SRInequality ineq1_2(EV1);
  EXPECT_TRUE(ineq1 == ineq1_2);  //Tests the equal to operator
}

//This tests the SRConjunction class and all of its methods except for the apply
//methods for the tree.
//Methods Tested:
//Less than operator:
//   The less than operator works by first checking the sizes of the sets inside
//   the SRConjunction, and then by applying the less than operator over the
//   sets themselves which will call the less than operators of the SREqualities
//   and the SRInequalities.
//Equal to operator:
//   The equal to operator works in the same fashion: checking the sizes of the
//   sets inside and then applying the equal to operator over the sets inside of
//   the SRConjunction
//isEmpty():
//   The isEmpty() method just checks the sizes of the sets to see if there
//   are no constraints actually in the conjunction.
TEST_F(SparseConstraintTest, ConjunctionTests){
  ExpVec EV1 = st->constructExpVec("var1", 4);
  ExpVec EV2 = st->constructExpVec("sym2", 3);
  ExpVec EV3 = st->constructExpVec("exist3", 2);
  ExpVec EV4 = st->constructExpVec("f()",list<ExpVec>(), 1);
  SREquality eq1(EV1);
  SREquality eq2(EV2);
  SRInequality ineq1(EV3);
  SRInequality ineq2(EV4);
  set<SREquality> eqs;
  eqs.insert(eq1);
  eqs.insert(eq2);
  set<SRInequality> ineqs;
  ineqs.insert(ineq1);
  ineqs.insert(ineq2);
  SRConjunction conj1(eqs, ineqs, tuples);
  SRConjunction conj2(eqs, ineqs, tuples);
  EXPECT_TRUE(conj1 == conj2);  //Tests the equal to operator

  ExpVec EV5 = st->constructExpVec("var2", 1);
  eqs.insert(SREquality(EV5));

  SRConjunction conj3(eqs, ineqs, tuples);
  EXPECT_TRUE(conj1 < conj3);   //Tests the less than operator

  EXPECT_FALSE(conj3.isEmpty());   //Tests the isEmpty method
}

//This tests the assertion statements in the Sparse_constraint class
//Since the asserts aren't in place yet (they're on the list of the test driven
//style and therefore commented out for now) this test case doesn't do much
//other than make sure that you can make a set or relation.
/*TEST_F(SparseConstraintTest, AssertionTests){
  ExpVec EV1 = st->constructExpVec("var1", 4);
  ExpVec EV2 = st->constructExpVec("sym2", 3);
  ExpVec EV3 = st->constructExpVec("exist3", 2);
  ExpVec EV4 = st->constructExpVec("f()",list<ExpVec>(), 1);
  SREquality eq1(EV1);
  SREquality eq2(EV2);
  SRInequality ineq1(EV3);
  SRInequality ineq2(EV4);
  set<SREquality> eqs;
  eqs.insert(eq1);
  eqs.insert(eq2);
  set<SRInequality> ineqs;
  ineqs.insert(ineq1);
  ineqs.insert(ineq2);
  SRConjunction conj1(eqs, ineqs, tuples);
  ExpVec EV5 = st->constructExpVec("var2", 1);
  eqs.insert(SREquality(EV5));
  SRConjunction conj2(eqs, ineqs, tuples);
  set<SRConjunction> conset;
  conset.insert(conj1);
  conset.insert(conj2);
  Set(st, conset, all, 3); //Should pass, both conjunctions present
                           //are using the same tuple list
  list<STE*> tuples2;
  tuples2.push_back(st->lookup("var1"));
  tuples2.push_back(st->lookup("var2"));
  SRConjunction conj3(eqs, ineqs, tuples2);
  conset.insert(conj3);
  //Should not pass, one conjunction present doesn't have the same tuple list
  Set(st, conset, all, 3);
}*/

//tests that the conjunction size is 1
TEST(ConCountTest, Set){
   Set PS1("{[x,y,z]:a<b and a<c}");
   EXPECT_EQ(PS1.conSize(), 1);

   Set PS2("{[x,x,x]:a<b and a<c}");
   EXPECT_EQ(PS2.conSize(), 1);

   Set PS3("{[x,x,x]:a<b and a<y}");
   EXPECT_EQ(PS3.conSize(), 1);
}

//tests that the conjucntion size is 1
TEST(ConCountTest, Relation){
   Relation PR1("{[x,y,z]->[a,b,c]}");
   EXPECT_EQ(PR1.conSize(), 1);

   Relation PR2("{[x,y,z]->[a,b,c]: a=10}");
   EXPECT_EQ(PR2.conSize(), 1);

   Relation PR3("{[x,y,z]->[a,b,c]: a=5 and z=6 and c<z}");
   EXPECT_EQ(PR3.conSize(), 1);
}

TEST(CopyTest, RelationcopyTest){
  Relation PR1("{[x,y,z]->[a,b,c]}");
  Relation PR2(PR1);
  EXPECT_EQ(PR2.get_isl(), "{[x,y,z]->[a,b,c]}");

  Relation PR3("{[x,x,x]->[a,b,c]}");
  Relation PR4 = PR3;
  EXPECT_EQ(PR4.get_isl(), "{[x,x1,x2]->[a,b,c] : x-x1=0 and x-x2=0}");
}

TEST(CopyTest, SetcopyTest){
  Set PS1("{[x,y,z]}");
  Set PS2(PS1);
  EXPECT_EQ(PS2.get_isl(), "{[x,y,z]}");

  Set PS3("{[x,x,x]}");
  Set PS4 = PS3;
  EXPECT_EQ(PS4.get_isl(), "{[x,x1,x2] : x-x1=0 and x-x2=0}");
}

TEST(CopyTest, RelationcopyTest2){
  Relation PR1("{[x,y,z]->[a,b,c]:a<y+4}");
  Relation PR2(PR1);
  EXPECT_EQ(PR2.get_isl(), "{[x,y,z]->[a,b,c] : -a+y+3>=0}");

  Relation PR3("{[x,x,x]->[a,b,c]: a-b+c>=0 && a>=10}");
  Relation PR4 = PR3;
  EXPECT_EQ(PR4.get_isl(),
    "{[x,x1,x2]->[a,b,c] : x-x1=0 and x-x2=0 and a-10>=0 and a-b+c>=0}");
}

TEST(CopyTest, SetcopyTest2){
  Set PS1("{[x,y,z]:z>x+y and x<0}");
  Set PS2(PS1);
  EXPECT_EQ(PS2.get_isl(), "{[x,y,z] : -x-y+z-1>=0 and -x-1>=0}");

  Set PS3("{[x,x,x1]:x1+3=x}");
  Set PS4 = PS3;
  Set PS4_expected("{[x,x1,x11] : x-x1-3=0 and x1-x11=0 and x-x1=0}");
  EXPECT_EQ(PS4, PS4_expected);
  EXPECT_EQ(PS4.get_isl(), "{[x,x1,x11] : 1=0}");
}

#if 0
TEST(MergeSymbolTableTest, SetTests){
  Set PS1("{[x]: a < 0}");
  Set PS2("{[y]: b > 0}");

  pair<SparseConstraints*, SparseConstraints*>
    intermediatePair = PS1.mergeSymbolTables(PS2);
  pair<Set*, Set*> final = make_pair(static_cast<Set*>(intermediatePair.first),
    static_cast<Set*>(intermediatePair.second));

  EXPECT_EQ(final.first->get_isl(), "{[x] : -a-1>=0}");
  EXPECT_EQ(final.second->get_isl(), "{[x] : b-1>=0}");

  delete final.first;
  delete final.second;

  Set PS3("{[x]: x < 0}");
  Set PS4("{[y]: y > 0}");

  intermediatePair = PS3.mergeSymbolTables(PS4);
  final = make_pair(static_cast<Set*>(intermediatePair.first),
    static_cast<Set*>(intermediatePair.second));

  EXPECT_EQ(final.first->get_isl(), "{[x] : -x-1>=0}");
  EXPECT_EQ(final.second->get_isl(), "{[x] : x-1>=0}");

  delete final.first;
  delete final.second;

  Set PS5("{[x]: x - a < 0}");
  Set PS6("{[y]: y - b> 0}");

  intermediatePair = PS5.mergeSymbolTables(PS6);
  final = make_pair(static_cast<Set*>(intermediatePair.first),
    static_cast<Set*>(intermediatePair.second));

  EXPECT_EQ(final.first->get_isl(), "{[x] : -x+a-1>=0}");
  EXPECT_EQ(final.second->get_isl(), "{[x] : x-b-1>=0}");

  delete final.first;
  delete final.second;
}

TEST(MergeSymbolTableTest, RelationTests){
  Relation PS1("{[x]->[y]: a < 0}");
  Relation PS2("{[y]->[z]: b > 0}");

  pair<SparseConstraints*, SparseConstraints*>
    intermediatePair = PS1.mergeSymbolTables(PS2);
  pair<Relation*, Relation*> final =
    make_pair(static_cast<Relation*>(intermediatePair.first),
      static_cast<Relation*>(intermediatePair.second));

  EXPECT_EQ(final.first->get_isl(), "{[x]->[y] : -a-1>=0}");
  EXPECT_EQ(final.second->get_isl(), "{[x]->[y] : b-1>=0}");

  delete final.first;
  delete final.second;

  Relation PS3("{[x]->[y]: x < 0}");
  Relation PS4("{[y]->[z]: y > 0}");

  intermediatePair = PS3.mergeSymbolTables(PS4);
  final = make_pair(static_cast<Relation*>(intermediatePair.first),
    static_cast<Relation*>(intermediatePair.second));

  EXPECT_EQ(final.first->get_isl(), "{[x]->[y] : -x-1>=0}");
  EXPECT_EQ(final.second->get_isl(), "{[x]->[y] : x-1>=0}");

  delete final.first;
  delete final.second;

  Relation PS5("{[c]->[d,e,f]: x < 0}");
  Relation PS6("{[y]->[z]: y > 0}");

  intermediatePair = PS5.mergeSymbolTables(PS6);
  final = make_pair(static_cast<Relation*>(intermediatePair.first),
    static_cast<Relation*>(intermediatePair.second));
  std::cout<<final.first->get_isl()<< " " << final.second->get_isl()<<std::endl;
  EXPECT_EQ(final.first->get_isl(), "{[x,y]->[i,j] : -x-1>=0}");
  EXPECT_EQ(final.second->get_isl(), "{[x]->[y] : x-1>=0}");

  delete final.first;
  delete final.second;
}

TEST(MergeSymbolTableTest, FunctionTests){
  Set PS1("{[x]: f(x) < 0}");
  Set PS2("{[y]: f(y) > 0}");

  pair<SparseConstraints*, SparseConstraints*> intermediatePair =
    PS1.mergeSymbolTables(PS2);
  pair<Set*, Set*> final = make_pair(static_cast<Set*>(intermediatePair.first),
    static_cast<Set*>(intermediatePair.second));

  EXPECT_EQ(final.first->get_isl(), "{[x] : -f(x)-1>=0}");
  EXPECT_EQ(final.second->get_isl(), "{[x] : f(x)-1>=0}");

  delete final.first;
  delete final.second;
}
#endif


TEST(SRConjunction, Rel){
    Relation PS1("{[x]->[y]: y < 0}");
    Relation PS2("{[x]->[y]: y < 0}");

    set<SRConjunction>::const_iterator itr1 = PS1.conSetBegin();
    set<SRConjunction>::const_iterator itr2 = PS2.conSetBegin();
    EXPECT_TRUE((*itr1)==(*itr2));
}

TEST(SRConjunction, Rel1){
    Relation PS1("{[x]->[y]: x < 0}");
    Relation PS2("{[x]->[y]: y < 0}");

    set<SRConjunction>::const_iterator itr1 = PS1.conSetBegin();
    set<SRConjunction>::const_iterator itr2 = PS2.conSetBegin();
    EXPECT_FALSE((*itr1)==(*itr2));
}

TEST(SRConjunction, set){
    Set PS1("{[i]: j > i}");
    Set PS2("{[i]: j > i}");

    set<SRConjunction>::const_iterator itr1 = PS1.conSetBegin();
    set<SRConjunction>::const_iterator itr2 = PS2.conSetBegin();
    EXPECT_EQ((*itr1)==(*itr2),true);
}

TEST(SRConjunction, set1){
    Set PS1("{[i]: j > 12}");
    Set PS2("{[i]: j > 9}");

    set<SRConjunction>::const_iterator itr1 = PS1.conSetBegin();
    set<SRConjunction>::const_iterator itr2 = PS2.conSetBegin();
    EXPECT_EQ((*itr1), (*itr2));
}

TEST(SRConjunction, set2){
    Set PS1("{[i]: j > k}");
    Set PS2("{[i]: j > i}");

    set<SRConjunction>::const_iterator itr1 = PS1.conSetBegin();
    set<SRConjunction>::const_iterator itr2 = PS2.conSetBegin();
    EXPECT_EQ((*itr1)==(*itr2),true);
}

TEST(SRConjunction, set3){
    Set PS1("{[j]: j > 9}");
    Set PS2("{[i]: i > 9}");

    set<SRConjunction>::const_iterator itr1 = PS1.conSetBegin();
    set<SRConjunction>::const_iterator itr2 = PS2.conSetBegin();
    EXPECT_TRUE((*itr1)==(*itr2));
}

TEST(SRConjunction, set4){
    Set PS1("{[x,y]: x > y}");
    Set PS2("{[x,y]: y > x}");

    set<SRConjunction>::const_iterator itr1 = PS1.conSetBegin();
    set<SRConjunction>::const_iterator itr2 = PS2.conSetBegin();
    EXPECT_FALSE((*itr1)==(*itr2));
}

TEST(SRConjunction, getInvFuncCandidate){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");

  set<string> tups,exists,syms;
  tups.insert("a");
  exists.insert("b");

  SymbolTable sym_table(&tups,&syms,&exists,2);

  ExpVec a_exp(sym_table.constructExpVec("a",1));
  ExpVec b_exp(sym_table.constructExpVec("b",1));

  UFCall *f_of_b=sym_table.lookup("f",list<ExpVec>(1,b_exp));
  UFCall *f_inv_of_a=sym_table.lookup("f_inv",list<ExpVec>(1,a_exp));

  ExpVec a_minus_f_of_b(sym_table.constructExpVec());
  a_minus_f_of_b.set_coeff(TUPLE,0,1);
  a_minus_f_of_b.set_coeff(UFCALL,0,-1);

  SREquality a_eq_f_of_b(a_minus_f_of_b);

  ExpVec f_of_a_minus_b(sym_table.constructExpVec());
  f_of_a_minus_b.set_coeff(UFCALL,1,1);
  f_of_a_minus_b.set_coeff(EXISTENTIAL,0,-1);

  SREquality f_of_a_eq_b(f_of_a_minus_b);

  SREquality orig_eq(sym_table.constructExpVec()),
             new_eq(sym_table.constructExpVec());

  set<SREquality> empty_eqs;
  SRConjunction empty_conj(empty_eqs,set<SRInequality>(),
                           list<TupleType>());
  EXPECT_FALSE(empty_conj.getInvFuncCandidate(&sym_table,context,orig_eq,new_eq));

  set<SREquality> eqs;
  eqs.insert(a_eq_f_of_b);
  SRConjunction conj(eqs,set<SRInequality>(),list<TupleType>());

  EXPECT_TRUE(conj.getInvFuncCandidate(&sym_table,context,orig_eq,new_eq));

  EXPECT_EQ(a_eq_f_of_b,orig_eq);
  EXPECT_EQ(f_of_a_eq_b,new_eq);
}

//Test for bug #410
TEST(NegationBug,test1){
  Set PS1("{[a]: -a=10}");
  Set PS2("{[a]: a=-10}");

  EXPECT_EQ(PS1,PS2);
}

/********** Simplification Tests **********/
TEST(Simplify, set1){
  Set PS1("{[x]: x=a and a=10}");
  Set PS2("{[y]: y=10}");

  EXPECT_EQ(PS1,PS2);
}

TEST(Simplify, rel1){
  Relation PR1("{[x]->[z]: x=a and a=10}");
  Relation PR2("{[y]->[z]: y=10}");

  EXPECT_EQ(PR1,PR2);
}

TEST(Simplify, set2){
  Set PS1("{[x]: x=b and b=a and a=10}");
  Set PS2("{[y]: y=10}");

  EXPECT_EQ(PS1,PS2);
}

TEST(Simplify, set3){
  Set PS1("{[x]: x<b and b=a and a=10}");
  Set PS2("{[y]: y<10}");

  EXPECT_EQ(PS1,PS2);
}

TEST(Simplify, set4){
  Set PS1("{[x]: x<b and x=f(a+5) and b=a and a=10}");
  Set PS2("{[y]: y<10 and y=f(15)}");

  EXPECT_EQ(PS1,PS2);
}

TEST(Simplify, set5){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  Set PS1("{[x]: x<e and 10=f(e)}",context);
  Set PS2("{[y]: y<f_inv(10)}",context);

  EXPECT_EQ(PS1,PS2);
}

TEST(Simplify, set6){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  Set PS1("{[x]: x<2e and 10=-1f(e)}",context);
  Set PS2("{[y]: y<2f_inv(-10)}",context);

  EXPECT_EQ(PS1,PS2)<<PS1.get_isl()<<"!="<<PS2.get_isl();
}

TEST(Simplify, set7){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  Set PS1("{[x,y]: 4x>3e+5 and 5y>2e+6 and f(2x+3y-e)=14-x+2y}",context);
  Set PS2("{[a,b]: -2a-9b+3f_inv(14-a+2b)-6>=0 and -4a-b+2f_inv(14-a+2b)-7>=0}",context);
  Set PS3("{[a,b]: 4a>6a+9b-3f_inv(14-a+2b)+5 and 5b>4a+6b-2f_inv(14-a+2b)+6}",context);

  EXPECT_EQ(PS1,PS3)<<PS1.get_isl()<<"!="<<endl<<PS3.get_isl();
  EXPECT_EQ(PS1,PS2)<<PS1.get_isl()<<"!="<<endl<<PS2.get_isl();
}

TEST(Simplify, set8){
  IEGenLibContext context;
  context.addSymbolic(Symbolic("n"));
  context.addInversePair("f","f_inv");
  Set PS1("{[a,b]: b<n and a=f(n)}",context);

  IEGenLibContext context2;
  context2.addInversePair("f","f_inv");
  Set PS2("[n]->{[a,b]: b<n and a=f(n)}",context2);

  EXPECT_EQ(PS1,PS2)<<PS1.get_isl()<<"!="<<endl<<PS2.get_isl();
}

TEST(Simplify, set9){
  Set PS1("{[a,b] : x=f(a,b) and a+b<=10 and f(a)=2b}");
  Set PS2("{[a,b] : 2b-f(a)=0 and -a-b+10>=0}");
  PS1.get_dot();
  EXPECT_EQ(PS1,PS2);
}

TEST(Simplify, set10){
  Set PS1("{[a,b,c,d] : a <= b-c and e = p(a,b,c*2,d,g(3),f(a+b)) }");
  Set PS2("{[a,b,c,d] : -a+b-c>=0}");
  PS1.get_dot();
  EXPECT_EQ(PS1,PS2);
}

TEST(Simplify, rel2){
  IEGenLibContext context;
  context.addSymbolic(Symbolic("n"));
  context.addInversePair("f","f_inv");
  Relation PR1("{[a]->[b]: b<n and a=f(n)}",context);

  IEGenLibContext context2;
  context2.addInversePair("f","f_inv");
  Relation PR2("[n]->{[a]->[b]: b<n and a=f(n)}",context2);

  EXPECT_EQ(PR1,PR2)<<PR1.get_isl()<<"!="<<endl<<PR2.get_isl();
}

TEST(Simplify, FuncNested){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  context.addInversePair("g","g_inv");
  Set set("{[a,b]: b<e and a=g(f(e))}",context);
  Set res("{[a,b] : -b+f_inv(g_inv(a))-1>=0}",context);

  //TODO: Need to add recursive support to ExpVec::any(SymType,int&,int&)
  //Should add optional SymbolTable=NULL argument and recurse if given
  //Should also update tests to make sure this change works
  EXPECT_EQ(set,res);
}

TEST(Simplify, FuncNested2){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  context.addInversePair("g","g_inv");
  context.addInversePair("q","q_inv");
  Set set("{[a,b]: b<e and a=q(g(f(e)))}",context);
  Set res("{[a,b] : -b+f_inv(g_inv(q_inv(a)))-1>=0}",context);

  EXPECT_EQ(set,res);
}

TEST(Simplify, FuncNested3){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  context.addInversePair("g","g_inv");
  context.addInversePair("q","q_inv");
  Set set("{[a,b]: a>=e and b=q(g(f(e)))}",context);
  Set res("{[a,b] : a-f_inv(g_inv(q_inv(b)))>=0}",context);

  EXPECT_EQ(set,res);
}

TEST(Simplify, FuncNested4){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  context.addInversePair("g","g_inv");
  context.addInversePair("q","q_inv");
  context.addInversePair("f2","f2_inv");
  Set set("{[a,b]: a>=e and b=f2(q(g(f(e))))}",context);
  Set res("{[a,b] : a-f_inv(g_inv(q_inv(f2_inv(b))))>=0}",context);

  EXPECT_EQ(set,res);
}

TEST(Simplify, FuncNoGo1){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  Set set("{[a,b]: b<e and a=2f(e)}",context);

  //TODO: This is a string test as we cannot currently compare two Sets
  // with different contexts to allow disabling of simplification in one set
  EXPECT_EQ(set.get_isl(),"{[a,b] : exists(e : a-2f(e)=0)}");
  // the expected result set updated, it was:
  // "{[a,b] : exists(e : a-2f(e)=0 and -b+e-1>=0)}"
}

TEST(Simplify, FuncNoGo2){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  Set set("{[a,b]: b<e and a=f(e,a)}",context);

  //TODO: This is a string test as we cannot currently compare two Sets
  // with different contexts to allow disabling of simplification in one set
  EXPECT_EQ(set.get_isl(),"{[a,b] : exists(e : a-f(e,a)=0)}");
  // the expected result set updated, it was:
  // "{[a,b] : exists(e : a-f(e,a)=0 and -b+e-1>=0)}"
}

TEST(Simplify, FuncNoGo3){
  IEGenLibContext context;
  Set set("{[a,b]: b<e and a=f(e)}",context);

  //TODO: This is a string test as we cannot currently compare two Sets
  // with different contexts to allow disabling of simplification in one set
  EXPECT_EQ(set.get_isl(),"{[a,b] : exists(e : a-f(e)=0)}");
  // the expected result set updated, it was:
  // "{[a,b] : exists(e : a-f(e)=0 and -b+e-1>=0)}"
}

TEST(Simplify, ContextUnionCompose){
  // test the case of union two different contexts of two Relations, when we
  // apply the Compose operation between them
  IEGenLibContext context;
  context.addSymbolic(Symbolic("n"));
  context.addInversePair("f","f_inv");
  Relation R1("{[0,i0,0]->[ar] : ar-f(i0)=0}", context);

  IEGenLibContext context2;
  context2.addSymbolic(Symbolic("m"));
  context2.addInversePair("f","f_inv");
  context2.addInversePair("cb","cb_inv");
  Relation R2("{[0,b,0,r,0,i,0]->[0,i,0] : r-f(i)=0 and b-cb(i)=0}", context2);

  Relation R3(R1.Compose(R2));
  
  IEGenLibContext context3;
  context3.addInversePair("f","f_inv");
  context3.addInversePair("cb","cb_inv");
  Relation R4("[n, m]->{[0,b,0,r,0,i0,0]->[ar] : r-f(i0)=0 and b-cb(i0)=0 and ar-f(i0)=0}", context3);

  EXPECT_EQ(R3,R4)<<R3.get_isl()<<"!="<<endl<<R4.get_isl();
}

TEST(Simplify, ContextUnionApply){
  // test the case of union two different contexts of Set and Relation,
  // when we apply the Apply operation between them
  IEGenLibContext context;
  context.addSymbolic(Symbolic("nnz"));
  context.addInversePair("row","row_inv");
  context.addInversePair("cb","cb_inv");
  Set S1("{[0,b,0,r,0,i0,0] : r-row(i0)=0 and b-cb(i0)=0 and nnz-i0>0 and i0>=0}", context);

  IEGenLibContext context2;
  context2.addInversePair("row","row_inv");
  Relation R1("{[0,b,0,r,0,i,0]->[b,r,i] : row(i)=2 }", context2);

  Set S2(R1.Apply(S1));

  IEGenLibContext context3;
  context3.addInversePair("row","row_inv");
  context3.addInversePair("cb","cb_inv");
  Set S3("[nnz]->{[b,r,i0] : r-row(i0)=0 and b-cb(i0)=0 and nnz-i0>0 and i0>=0 and row(i0)=2}", context3);

  EXPECT_EQ(S2,S3)<<S2.get_isl()<<"!="<<endl<<S3.get_isl();
}

TEST(Simplify, ContextUnionRelation){
  // test the case of union two different contexts of Relations,
  // when we apply the Union operation between them

  IEGenLibContext context;
  context.addSymbolic(Symbolic("n"));
  context.addInversePair("f","f_inv");
  Relation R1("{[a,i0,0]->[ar] : a=0 and ar-f(i0)=0}", context);

  IEGenLibContext context2;
  context2.addSymbolic(Symbolic("m"));
  context2.addInversePair("f","f_inv");
  context2.addInversePair("cb","cb_inv");
  Relation R2("{[r,i,0]->[i] : r-f(i)=0 and b-cb(i)=0}", context2);

  Relation R3(R1.Union(R2));
  
  IEGenLibContext context3;
  context3.addInversePair("f","f_inv");
  context3.addInversePair("cb","cb_inv");
  Relation R4("[n, m]->{[r,i,0]->[i] : r-f(i)=0 and b-cb(i)=0; [a,i0,0]->[ar] : a=0 and ar-f(i0)=0}", context3);

  EXPECT_EQ(R3,R4)<<R3.get_isl()<<"!="<<endl<<R4.get_isl();
}

TEST(Simplify, ContextUnionSet){
  // test the case of union two different contexts of Sets,
  // when we apply the Union operation between them

  IEGenLibContext context;
  context.addSymbolic(Symbolic("n"));
  context.addInversePair("f","f_inv");
  Set S1("{[ar,i0,b] : ar-f(i0)=0}", context);

  IEGenLibContext context2;
  context2.addSymbolic(Symbolic("m"));
  context2.addInversePair("f","f_inv");
  context2.addInversePair("cb","cb_inv");
  Set S2("{[r,i,b] : r-f(i)=0 and b-cb(i)=0}", context2);

  Set S3(S1.Union(S2));
  
  IEGenLibContext context3;
  context3.addInversePair("f","f_inv");
  context3.addInversePair("cb","cb_inv");
  Set S4("[n, m]->{[ar,i0,b] : ar-f(i0)=0; [r,i,b] : r-f(i)=0 and b-cb(i)=0}", context3);

  EXPECT_EQ(S3,S4)<<S3.get_isl()<<"!="<<endl<<S4.get_isl();
}

TEST(Simplify, SimplifyFuncFuncinv1){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  context.addInversePair("g","g_inv");
  Set set("{[a,b]: b<a and a=g(g_inv(f(b)))}",context);
  Set res("{[a,b] : b<a and a-f(b)=0}",context);
  EXPECT_EQ(set,res);

  Set set2("{[a,b]: b<a and a=g_inv(g(f(b)))}",context);
  Set res2("{[a,b] : b<a and a-f(b)=0}",context);
  EXPECT_EQ(set2,res2);

  Set set3("{[a,b]: b<a and a+f_inv(f(b))=g_inv(g(f(b)))}",context);
  Set res3("{[a,b] : b<a and a+b-f(b)=0}",context);
  EXPECT_EQ(set3,res3);
}

TEST(Simplify, SimplifyFuncFuncinv2){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  context.addInversePair("g","g_inv");
  Set set4("{[a,b]: b<a and a+f_inv(f(b))=g_inv(g(f(b))) and f(f_inv(g_inv(g(b))))=f(b)}",context);
  Set res4("{[a,b] : b<a and a+b-f(b)=0 and b=f(b)}",context);
  EXPECT_EQ(set4,res4);

  Set set5("{[a,b]: b<a and a+f_inv(g(b))=g_inv(g(f(b))) and f(g_inv(g_inv(f(b))))=f(b)}",context);
  Set res5("{[a,b] : b<a and a+f_inv(g(b))-f(b)=0 and f(g_inv(g_inv(f(b))))=f(b)}",context);
  EXPECT_EQ(set5,res5);

  Set set6("{[a,b]: b<a and a=g(g_inv(f(b))+a)}",context);
  Set res6("{[a,b] : b<a and a-g(g_inv(f(b))+a)=0}",context);
  EXPECT_EQ(set6,res6);
}

TEST(Simplify, SimplifyFuncFuncinv3){
  IEGenLibContext context;
  context.addInversePair("f","f_inv");
  context.addInversePair("g","g_inv");
  Set set7("{[a,b,c]: b<a and a=g(g_inv(f(b)+f(c)))}",context);
  Set res7("{[a,b,c] : b<a and a-(f(b)+f(c))=0}",context);
  EXPECT_EQ(set7,res7);

  Set set8("{[a,b,c]: b<a and a=g(g_inv(f(b))+f(c))}",context);
  Set res8("{[a,b,c] : b<a and a-g(g_inv(f(b))+f(c))=0}",context);
  EXPECT_EQ(set8,res8);

  Set set9("{[a,b,c]: b<a and a=g(g_inv(f_inv(f(c))))}",context);
  Set res9("{[a,b,c] : b<a and a-c=0}",context);
  EXPECT_EQ(set9,res9);

  Set set10("{[a,b,c]: b<a and a=g(g_inv(f_inv(f(c-b))))}",context);
  Set res10("{[a,b,c] : b<a and a-c+b=0}",context);
  EXPECT_EQ(set10,res10);
}
/******************************************/
